d-world-state(D;i)
== :M(i).(timed)state  (:Action(d-decl(D;i))  ({m:M(i).Msg| source(mlnk(m)) = i}  List)) 

latex

---

clarification:

d-world-state(D;i)
== :d-m(D; i).(timed)state
==  (:Action(d-decl(D;i))
==  ({m:d-m(D; i).Msg| source(mlnk(m)) = i  Id}  List)) 

latex

Definitions	x:A  B(x), Action(dec), d-decl(D;i), type List, {x:A| B(x)} , M.Msg, M(i), s = t, Id, source(l), mlnk(m)
FDL editor aliases	d-world-state